COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Ma Xiwen's axioms for Mr. S and Mr. P which are a variant of an
C00004 00003	DECLARE INDVAR t ε NATNUM
C00008 00004	# LEMMA 1
C00019 ENDMK
C⊗;
Ma Xiwen's axioms for Mr. S and Mr. P which are a variant of an
earlier version by McCarthy.

 	 This is an approach to the axiomatization of Mr.S and Mr.P.
      	Its basic idea is the same of KNOW[E78,JMC].                  
	 These are some diffrent symbols:
 
		k	for a PAIR of NATNUMs
		s(k)    for the sum of the two NATNUM in k
		p(k)    for the product of the two NATNUM in k
	
	 We have introduced a few of PREDCONSTs, for abbreviation only.
    	 But there are some important differences between the two 
	axiomatizations: our axiom SP is weaker, but our axioms LP
	and LS are stronger.
 	 The PREDCONSTs R1 R2 and R3 are slightly different,too.
	
	 Next follws a complete list of commands of the FOL proof of
	R3(k0). The subsequent proof that k0=<4,13> will be purely
	arithmetic, and a computer search has been done to confirm
	it.

	 


I have changed the learning axioms LP and LS, and I have removed
the redundant predicate OK.  Where I have times 1 and 2 in
A(RW,w,SP,n), Ma had 0.  I think these axioms are too strong and
may even make the system inconsistent.  I don't know whether Ma's
proof will work with the weaker axioms.  - JMC
DECLARE INDVAR t ε NATNUM;
DECLARE INDCONST k0 ε PAIR;
DECLARE INDVAR k k1 k2 k3 ε PAIR;
DECLARE INDCONST RW ε WORLD;
DECLARE INDVAR w w1 w2 w3 ε WORLD;
DECLARE INDCONST S P SP ε PERSON;
DECLARE INDVAR r ε PERSON;
DECLARE OPCONST K(WORLD)=PAIR;  
DECLARE OPCONST s(PAIR)=NATNUM;
DECLARE OPCONST p(PAIR)=NATNUM;
DECLARE PREDCONST A(WORLD,WORLD,PERSON,NATNUM);
DECLARE PREDCONST Qs(PAIR) Qp(PAIR) Q1(PAIR) Q2(PAIR) Q3(PAIR);
DECLARE PREDCONST Bs(WORLD) Bp(WORLD) B1(WORLD) B2(WORLD);
DECLARE PREDCONST R1(PAIR) R2(PAIR) R3(PAIR);
DECLARE PREDCONST C1(WORLD) C2(WORLD);

AXIOM AR: ∀w r t.A(w,w,r,t);;
AXIOM AT: ∀w1 w2 w3 r t.(A(w1,w2,r,t)∧A(w2,w3,r,t)⊃A(w1,w3,r,t));;
AXIOM SP: ∀w1 w2 t.(A(w1,w2,S,t)∨A(w1,w2,P,t)⊃A(w1,w2,SP,t));;
AXIOM RW: k0=K(RW);;
AXIOM INIT:
    	∀w w1.(A(RW,w,SP,0)∧A(w,w1,S,0)⊃s(K(w))=s(K(w1))),
	∀w w1.(A(RW,w,SP,0)∧A(w,w1,P,0)⊃p(K(w))=p(K(w1))),
    	∀w k.(A(RW,w,SP,0)∧s(K(w))=s(k)⊃∃w1.(A(w,w1,S,0)∧k=K(w1))),
	∀w k.(A(RW,w,SP,0)∧p(K(w))=p(k)⊃∃w1.(A(w,w1,P,0)∧k=K(w1)));;

AXIOM R:
	∀k.(R1(k)≡Qs(k)∧Q1(k)),
	∀k.(R2(k)≡R1(k)∧Q2(k)),
	∀k.(R3(k)≡R2(k)∧Q3(k));;
AXIOM BS: ∀w.(Bs(w)≡∃w1.(A(w,w1,S,0)∧¬(K(w)=K(w1))));;
AXIOM BP: ∀w.(Bp(w)≡∃w1.(A(w,w1,P,0)∧¬(K(w)=K(w1))));;
AXIOM B:
	∀w.(B1(w)≡∀w1.(A(w,w1,S,0)⊃Bp(w1))),
	∀w.(B2(w)≡∀w1.(A(w,w1,P,1)⊃K(w)=K(w1)));;
AXIOM C:
	∀w.(C1(w)≡Bs(w)∧B1(w)),
	∀w.(C2(w)≡C1(w)∧B2(w));;
AXIOM SKNPK: B1(RW);;
AXIOM NSK:   Bs(RW);;
AXIOM PK:    B2(RW);;
AXIOM SK:    ∀w.(A(RW,w,S,2)⊃K(RW)=K(w));;
AXIOM LP: ∀w w1.(A(RW,w,SP,1)⊃(A(w,w1,P,1)≡A(w,w1,P,0)∧C1(w1)));;
AXIOM LS: ∀w w1.(A(RW,w,SP,2)⊃(A(w,w1,S,2)≡A(w,w1,S,1)∧C2(w1)));;

AXIOM QS: ∀k.(Qs(k)≡∃k1.(s(k)=s(k1)∧¬(k=k1)));;
AXIOM QP: ∀k.(Qp(k)≡∃k1.(p(k)=p(k1)∧¬(k=k1)));;
AXIOM Q:
	∀k.(Q1(k)≡∀k1.(s(k)=s(k1)⊃Qp(k1))),
	∀k.(Q2(k)≡∀k1.(R1(k1)∧p(k)=p(k1)⊃k=k1)),
	∀k.(Q3(k)≡∀k1.(R2(k1)∧s(k)=s(k1)⊃k=k1));;

COMMENT # LEMMA 1
	∀w k.(A(RW,w,SP,0)∧k=K(w)⊃(Qs(k)≡Bs(w))) 
COMMENT # LEMMA 2
        ∀w k.(A(RW,w,SP,0)∧k=K(w)→(Qp(k)≡Bp(w)))
COMMENT # LEMMA 3
	∀w k.(A(RW.w.SP,0)∧k=K(w)→(Q1(k)≡B1(w)))
COMMENT # LEMMA 4
	∀w k.(A(RW,w,SP,0)∧k=K(w)⊃(R1(k)≡C1(w)))
COMMENT # LEMMA 5
	R2(k0)
COMMENT # LEMMA 6
	∀w k.(A(RW,w,SP,0)∧k=K(w)⊃(R2(k)⊃C2(w)))
COMMENT # LEMMA 7
      	Q3(k0)
COMMENT # MAIN THEOREM
	R3(k0)